package edu.uclm.combTest.core;

import java.util.Iterator;

public class OrderedVector implements java.lang.Iterable {
	protected /*@ spec_public @*/ Vector elementos;

	//@ public invariant 
	//@ (\forall int i ; i>=0 && i<elementos.size() ; 
	//@ (\forall int j ; j>=0 && j<elementos.size() ;
	//@ (i<j ==> ((Long)elementos.get(i)).longValue() < ((Long)elementos.get(j)).longValue() 
	//@)));
	
	//@ensures elementos.size()==0;
	public OrderedVector() {
		this.elementos=new Vector();
	}
	
	
	//soit il contenait déja l'élément
	//@requires(elementos.contains(new Long(n)));
	//@also
	//soit il contient 1 element un plus
	//@requires(!elementos.contains(new Long(n)));
	//@ensures(elementos.size() == \old(elementos.size()+1));
	//@ensures(elementos.contains(new Long(n)));
	//contient tous les elements qu'il contenait avant.
	//@ensures(\forall int i ; i>=0 && i < \old(elementos.size()) ; (
	//@	elementos.contains((Long)\old(elementos.get(i)))
	//@));
	public void add(long n) {
		if (this.contains(n, 0, this.elementos.size()-1))
			return;
		if (this.elementos.size()==0) {
			this.elementos.add(new Long(n));
			return;
		}
		if (((Long)this.elementos.lastElement()).longValue()<n) {
			this.elementos.add(new Long(n));
			return;
		}
		int pos=this.findPos(n);
		this.elementos.insertElementAt(new Long(n), pos);
	}

/**
 * Contient une valeur entre 2 indices a et b ?
 * @param n  valeur
 * @param a l'indice a (peut etre <0 ou > size)
 * @param b l'indice b (peut etre <0 ou > size)
 * @return vrai si la valeur est présente entre a et b
 */

//@ensures (\result == (\exists
//@ int i ; i>=a && i <= b ; (((Long)elementos.get(i)).longValue() == n)
//@));

	protected /*@ pure @*/ boolean contains(long n, int a, int b) {
		if (a>b)
			return false;
		int mitad=(a+b)/2;
		if (((Long)this.elementos.get(mitad)).longValue()==n)
			return true;
		if (((Long)this.elementos.get(mitad)).longValue()>n)
			return this.contains(n, a, mitad-1);
		else return this.contains(n, mitad+1, b);
	}

	public /*@ pure @*/ synchronized String toString() {
		String r="";
		for (int i=0; i<this.elementos.size(); i++)
			r+=this.elementos.get(i)+"-";
		return r;
	}

	//@ensures \result != 0 ==> ((Long)elementos.get(\result-1)).longValue()<=n;
	//@ensures elementos.size() != \result ==>((Long)elementos.get(\result)).longValue()>=n;
	public/*@ pure @*/ int findPos(long n) {
		int a=0, b=this.elementos.size()-1, mitad, pos=-1;
		if (this.elementos.size()==0) {
			pos=0;
		} else if (((Long)this.elementos.get(b)).longValue()<n) {
			pos=b+1;
		}
		while (a<=b) {
			mitad=(a+b)/2;
			long elemento=((Long)this.elementos.get(mitad)).longValue();
			if (elemento==n)
				pos=mitad;
			else if (elemento<n)
				a=mitad+1;
			else
				b=mitad-1;
		}
		pos=a;
		return pos;
	}

	//@ensures \result == elementos.size();
	public /*@ pure @*/ int size() {
		return this.elementos.size();
	}

	////@Override
	public Iterator iterator() {
		return this.elementos.iterator();
	}

}
